<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Indenting7</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
\usepackage{agda}
\begin{document}

</a><a id="61" class="Markup">\begin{code}</a>
<a id="74" class="Keyword">module</a> <a id="81" href="Indenting7.html" class="Module">Indenting7</a> <a id="92" class="Keyword">where</a>

  <a id="101" class="Keyword">module</a> <a id="A₁"></a><a id="108" href="Indenting7.html#108" class="Module">A₁</a> <a id="111" class="Keyword">where</a>
  <a id="119" class="Keyword">module</a> <a id="A₂"></a><a id="126" href="Indenting7.html#126" class="Module">A₂</a> <a id="129" class="Keyword">where</a>

    <a id="140" class="Keyword">module</a> <a id="A₂.B₁"></a><a id="147" href="Indenting7.html#147" class="Module">B₁</a> <a id="150" class="Keyword">where</a>
    <a id="160" class="Keyword">module</a> <a id="A₂.B₂"></a><a id="167" href="Indenting7.html#167" class="Module">B₂</a> <a id="170" class="Keyword">where</a>

      <a id="183" class="Keyword">module</a> <a id="A₂.B₂.C₁"></a><a id="190" href="Indenting7.html#190" class="Module">C₁</a> <a id="193" class="Keyword">where</a>
      <a id="205" class="Keyword">module</a> <a id="A₂.B₂.C₂"></a><a id="212" href="Indenting7.html#212" class="Module">C₂</a> <a id="215" class="Keyword">where</a>

        <a id="230" class="Keyword">module</a> <a id="A₂.B₂.C₂.D₁"></a><a id="237" href="Indenting7.html#237" class="Module">D₁</a> <a id="240" class="Keyword">where</a>
        <a id="254" class="Keyword">module</a> <a id="A₂.B₂.C₂.D₂"></a><a id="261" href="Indenting7.html#261" class="Module">D₂</a> <a id="264" class="Keyword">where</a>

      <a id="277" class="Keyword">module</a> <a id="A₂.B₂.C₃"></a><a id="284" href="Indenting7.html#284" class="Module">C₃</a> <a id="287" class="Keyword">where</a>
      <a id="299" class="Keyword">module</a> <a id="A₂.B₂.C₄"></a><a id="306" href="Indenting7.html#306" class="Module">C₄</a> <a id="309" class="Keyword">where</a>

  <a id="318" class="Keyword">module</a> <a id="A₃"></a><a id="325" href="Indenting7.html#325" class="Module">A₃</a> <a id="328" class="Keyword">where</a>
    <a id="338" class="Keyword">module</a> <a id="A₃.B₃"></a><a id="345" href="Indenting7.html#345" class="Module">B₃</a> <a id="348" class="Keyword">where</a>
      <a id="360" class="Keyword">module</a> <a id="A₃.B₃.C₅"></a><a id="367" href="Indenting7.html#367" class="Module">C₅</a> <a id="370" class="Keyword">where</a>
        <a id="384" class="Keyword">module</a> <a id="A₃.B₃.C₅.D₃"></a><a id="391" href="Indenting7.html#391" class="Module">D₃</a> <a id="394" class="Keyword">where</a>
      <a id="406" class="Keyword">module</a> <a id="A₃.B₃.C₆"></a><a id="413" href="Indenting7.html#413" class="Module">C₆</a> <a id="416" class="Keyword">where</a>
    <a id="426" class="Keyword">module</a> <a id="A₃.B₄"></a><a id="433" href="Indenting7.html#433" class="Module">B₄</a> <a id="436" class="Keyword">where</a>
  <a id="444" class="Keyword">module</a> <a id="A₄"></a><a id="451" href="Indenting7.html#451" class="Module">A₄</a> <a id="454" class="Keyword">where</a>
<a id="460" class="Markup">\end{code}</a><a id="470" class="Background">

\end{document}
</a></pre></body></html>